(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 14))
(declare-fun v1 () (_ BitVec 12))
(declare-fun v2 () (_ BitVec 10))
(declare-fun v3 () (_ BitVec 14))
(assert (let ((e4(_ bv43824 16)))
(let ((e5(_ bv1815 11)))
(let ((e6 (bvsub v2 v2)))
(let ((e7 (bvmul ((_ sign_extend 2) v2) v1)))
(let ((e8 (bvshl ((_ zero_extend 1) v2) e5)))
(let ((e9 (ite (bvule ((_ zero_extend 4) e6) v3) (_ bv1 1) (_ bv0 1))))
(let ((e10 (bvor ((_ sign_extend 11) e9) e7)))
(let ((e11 ((_ repeat 1) e8)))
(let ((e12 (bvsub v1 e10)))
(let ((e13 ((_ repeat 1) e10)))
(let ((e14 (ite (bvsle ((_ sign_extend 2) v2) e12) (_ bv1 1) (_ bv0 1))))
(let ((e15 (ite (bvult e7 e13) (_ bv1 1) (_ bv0 1))))
(let ((e16 (bvurem ((_ zero_extend 2) v0) e4)))
(let ((e17 (bvsle ((_ sign_extend 1) v2) e5)))
(let ((e18 (bvsle ((_ sign_extend 1) e11) e7)))
(let ((e19 (bvsgt e13 e7)))
(let ((e20 (bvult e8 e11)))
(let ((e21 (bvsge e7 v1)))
(let ((e22 (= e12 e7)))
(let ((e23 (bvugt ((_ zero_extend 1) e6) e5)))
(let ((e24 (= e6 ((_ sign_extend 9) e9))))
(let ((e25 (bvult ((_ sign_extend 2) e6) e13)))
(let ((e26 (bvule ((_ sign_extend 2) v0) e16)))
(let ((e27 (bvule ((_ sign_extend 1) v2) e5)))
(let ((e28 (bvult e8 ((_ zero_extend 10) e9))))
(let ((e29 (bvslt ((_ sign_extend 3) e5) v3)))
(let ((e30 (bvsge ((_ sign_extend 2) e7) v3)))
(let ((e31 (bvsge v1 e13)))
(let ((e32 (distinct v3 ((_ sign_extend 3) e8))))
(let ((e33 (bvult e4 ((_ zero_extend 15) e14))))
(let ((e34 (bvult e8 e5)))
(let ((e35 (bvuge ((_ sign_extend 11) e14) v1)))
(let ((e36 (bvslt e16 ((_ sign_extend 5) e5))))
(let ((e37 (bvugt v3 ((_ zero_extend 3) e8))))
(let ((e38 (bvuge ((_ zero_extend 4) e6) v3)))
(let ((e39 (bvule e11 ((_ zero_extend 1) e6))))
(let ((e40 (bvult ((_ sign_extend 2) v0) e4)))
(let ((e41 (distinct e4 ((_ sign_extend 4) e13))))
(let ((e42 (bvsle e13 e7)))
(let ((e43 (bvsge ((_ zero_extend 1) e8) e10)))
(let ((e44 (bvsgt v1 v1)))
(let ((e45 (distinct e15 e14)))
(let ((e46 (xor e19 e30)))
(let ((e47 (xor e21 e17)))
(let ((e48 (ite e35 e31 e39)))
(let ((e49 (=> e37 e27)))
(let ((e50 (and e38 e49)))
(let ((e51 (and e47 e42)))
(let ((e52 (not e51)))
(let ((e53 (= e36 e25)))
(let ((e54 (or e22 e33)))
(let ((e55 (not e24)))
(let ((e56 (= e23 e48)))
(let ((e57 (ite e26 e55 e46)))
(let ((e58 (xor e40 e43)))
(let ((e59 (= e56 e44)))
(let ((e60 (=> e58 e18)))
(let ((e61 (ite e28 e28 e52)))
(let ((e62 (and e50 e59)))
(let ((e63 (or e20 e57)))
(let ((e64 (or e29 e60)))
(let ((e65 (and e32 e34)))
(let ((e66 (=> e54 e62)))
(let ((e67 (xor e61 e63)))
(let ((e68 (= e67 e67)))
(let ((e69 (ite e65 e68 e64)))
(let ((e70 (= e53 e45)))
(let ((e71 (= e69 e69)))
(let ((e72 (ite e70 e71 e71)))
(let ((e73 (= e41 e72)))
(let ((e74 (xor e66 e73)))
(let ((e75 (and e74 (not (= e4 (_ bv0 16))))))
e75
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
